Nuprl Lemma : div_nrel_wf
13,42
postcript
pdf
a
:
,
n
:
,
q
:
. Div(
a
;
n
;
q
)
latex
Up
int
2
,
int
2
Definitions
P
&
Q
,
i
j
<
k
,
Div(
a
;
n
;
q
)
,
,
t
T
,
x
:
A
.
B
(
x
)
,
,
Lemmas
nat
wf
,
nat
plus
wf
,
le
wf
origin
a:
, n:
, q:. Div(a;n;q) 
a:, n:, q:. Div(a;n;q) 
j < k Tx:A. B(x)